g:OMon. (a:|g|. monot(|g|;x,y.x < y;z.a * z))  {a:|g|. monot(|g|;x,y.x  y;z.a * z)} 

latex

Up	groups 1
Definitions of Statement	Mon, AbMon, OMon
Definitions	, t  T, {T}, x f y, monot(T;x,y.R(x;y);f), P  Q, x:A. B(x), P & Q, P  Q, P  Q, Mon, AbMon, OMon, P  Q
Lemmas	omon wf, grp op wf, grp lt wf, grp car wf, grp leq wf, grp leq iff lt or eq, grp leq weakening lt, grp leq weakening eq